package interfaces.gestores;

import interfaces.ICliente;
import tdg.contract.semanticAnnotations.Model;
import tdg.contract.semanticAnnotations.Query;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Pos;

public interface IGestorClientesWithModel extends IGestorClientes,
		IGestorClientesModel {
	@Pre ({"c!=null #NullPointerException","!clienteRegistrado(c)"})
	@Pos ({"clienteRegistrado(c)"})
	public void altaCliente(ICliente c);
	
	@Pre ({"c!=null #NullPointerException", "clienteRegistrado(c)"})
	@Pos ({"!clienteRegistrado(c)"})
	public void bajaCliente(ICliente c);
	
	@Pre ({"c1!=null && c2!=null #NullPointerException","clienteRegistrado(c1) && c1.getDni().equals(c2.getDni())"})
	@Pos ({"!clienteRegistrado(c1) && clienteRegistrado(c2)"})
	public void modificacionCliente(ICliente c1, ICliente c2);
}
